COMMENT ⊗   VALID 00016 PAGES
C REC  PAGE   DESCRIPTION
C00001 00001
C00003 00002	.require "memo.pub" source
C00004 00003	.<<cb REPRESENTATION OF RECURSIVE PROGRAMS IN FIRST ORDER LOGIC>>
C00016 00004	.bb "#. Recursive Programs."
C00024 00005	.bb "#. Two Useful Extensions to First Order Logic."
C00035 00006	.bb "#. Partial Functions and Partial Predicates."
C00047 00007	.bb "#. The Functional Equation of a Recursive Program - Theory."
C00059 00008	.bb "#. Axioms for S-expressions, Lists and Integers."
C00069 00009	.bb "#. Forms of Induction."
C00079 00010	.bb "#. An Extended Example."
C00087 00011	.bb "#. The Minimization Schema."
C00093 00012	.bb "#. Derived Programs and Complete Recursive Programs."
C00101 00013	.bb "#. Proof Methods as Axiom Schemata"
C00109 00014	.bb "#. Representations Using Finite Approximations."
C00115 00015	.BB "#. Questions of Incompleteness."
C00122 00016	.bb "#. References."
C00130 ENDMK
C⊗;
.require "memo.pub" source;
.<<every heading (RECURSIVE PROGRAMS,Cartwright and McCarthy,)>>
.every footing (,{page},)
.font B "zero30"
.AT "qt" ⊂"%At%*"⊃
.AT "qf" ⊂"%Af%*"⊃
.AT "qF" ⊂"%AF%*"⊃
.AT "qb" ⊂"%8T%*"⊃
.at "Goedel" ⊂"G%B:%*odel"⊃
.at "q≤" ⊂"%8b%*"⊃
.at "q≥" ⊂"%8d%*"⊃
.at "q<" ⊂"%8a%*"⊃
.at "q>" ⊂"%8c%*"⊃
.at "qx" ⊂"%8x%*"⊃
.at "qnil" ⊂"%1NIL%*"⊃
.at "qNIL" ⊂"%1NIL%*"⊃
.at "qw" ⊂"%Aw%*"⊃
.TURN ON "↑↓"
.select 1
.next page

.<<cb REPRESENTATION OF RECURSIVE PROGRAMS IN FIRST ORDER LOGIC>>
.cb RECURSIVE PROGRAMS AS FUNCTIONS IN A FIRST ORDER THEORY

.cb by Robert Cartwright and John McCarthy
.skip 5
%3Abstract%1

	Pure Lisp style recursive function programs are represented in a
new way by sentences and schemata of first order logic.  This permits easy
and natural proofs of extensional properties of such programs by methods
that generalize structural induction.  It also
systematizes known methods such as %2recursion induction%1, %2subgoal
induction%1, %2inductive assertions%1 by interpreting them as first
order axiom schemata.  We discuss the metatheorems
justifying the representation and techniques for proving facts about
specific programs.  We also give a simpler version of the Goedel-Kleene
way of representing computable functions by first order sentences.

%2	This research was supported by the Advanced Research Projects Agency
of the Department of Defense under contract MDA903-76-C-0206 and by the National
Science Foundation under grant NSF MCS 78-00524.
The views and conclusions contained in this document are those of the
authors and should not be interpreted as necessarily representing the
official policies, either expressed or implied, of Stanford University,
or any agency of the U. S. Government.%1

.bb "#. Introduction and Motivation."

	This paper advances two aspects of the study of the
properties of computer programs - the scientifically motivated search for
general theorems that permit deducing properties of programs and the
engineering problem of replacing debugging by computer-assisted
computer-checked proofs that programs have desired properties.
Both tasks require mathematics, but the second also requires keeping
a non-mathematical goal in mind - getting short completely formal
proofs that are easy to write and check by computer.

	A pure Lisp style recursive program ⊗P defines a partial function
%2f%4P%1.  By adjoining an undefined element qb (read "bottom") to the data
domains, %2f%4P%1 may be extended to a total function which we denote by the
same symbol.
In (Cartwright 1976), it was shown that %2f%4P%1 satisfies
a %2functional equation%1, which is a sentence in a first order theory %2T%4P%1.
Besides the functional equation,
%2T%4P%1 contains symbols for the basic functions, predicates and
constants of the data domain, axioms for the data domain and its extension
by qb, and additional function symbols for the functions defined
by recursive programs.  (Cartwright 1976) also showed how the functional
equation can be used to prove facts about the program by reasoning
within %2T%4P%1, including the fact that %2f%4P%1 is total, i.e. doesn't
take the value qb except when qb is an argument.

	When %2f%4P%1 is total, and sometimes when it isn't, it is
completely characterized by the functional equation.  Otherwise, the
characterization can be completed by a %2minimization schema%1 (McCarthy
1978 and this paper) or alternatively by a %2complete recursive function%1
as first defined in (Cartwright 1978).  Moreover,
we show how to find a representation of %2f%4P%1
by a sentence of the form %2(∀x)(y_=_f%4P%2(x)_≡_A(x))%1 where ⊗A(x) is a wff
of %2T%4P%1 not involving %2f%4P%1. 

	Now assume that %2T%4P%1 contains functions sufficient for axiomatizing
basic syntax, e.g. Lisp or elementary number theory, and let ⊗S be a
sentence of %2T%4P%1 involving only %2f%4P%1 and the basic functions of the data
domain.  Then (Cartwright and McCarthy 1979) shows how to construct a
sentence ⊗S' involving only the basic functions of the data domain such
that we can prove in first order logic that %2S_≡_S'%1.  Therefore, the
fact that total correctness is not axiomatizable in first order logic is
just a matter of the Goedelian incompleteness of the data domain, and it
can be expected that all "ordinary" facts about programs will be provable
just as all "ordinary" facts of elementary number theory are provable in
spite of its incompleteness.

	This paper is primarily concerned with proving such "ordinary"
facts about recursive function programs with a view to developing
practical techniques for program verification using interactive theorem
provers.  As such it should be compared with other ways of using logic
in program proving.

	Axiomatizing programs as functions compares favorably with
Floyd-Hoare methods in several respects.  First it permits stating
and proving facts that cannot even be stated in Floyd-Hoare formalisms
such as equivalence of programs and algebraic relations between
the functions defined by programs.  It has the advantage compared
to the Scott-Strachey formalisms that it uses ordinary first order
logic rather than a logic of continuous functions.  This permits
the use of any mathematical facts that can be expressed in first
order logic, including those that are most conveniently expressed in
set theory.  This is especially important when the statement of
program correctness or its informal proof involve other mathematical
objects than those that occur in the program data domain.

	After an informal introduction to recursive programs,
subsequent sections of this paper discuss the use of conditional
expressions and first order lambdas in first order logic, adjoining qb
to the data domains in order to convert partial functions and predicates
into total functions, axioms for Lisp and the integers, the representation
of recursive programs by functions, inductive methods of proof,
the minimization schema,
an extended example of a correctness proof, 
representation of the inductive assertion and subgoal induction methods
as axiom schemata, and a convenient way of representing recursively
defined functions by non-recursive sentences.

	Our methods apply directly to proving only ⊗extensional properties
of programs, e.g. properties of the function defined by the program.
Intensional properties such as the number of times an operation like
recursion or ⊗cons is performed are often extensional properties of
simply obtained %2derived programs%1.  Some of these properties are
also extensional properties of the functional of which the function is
the least fixed point.

	An adequate background for this paper is contained in (Manna 1974)
and more concisely in (Manna, Ness and Vuillemin 1973).  The connections
of recursive programs with second order logic are given in (Cooper 1969)
and (Park 1970).  Our notation differs from Manna's in order to
use the = sign exactly as in first order logic.
.bb "#. Recursive Programs."

	We consider recursive programs like

%2Factorial:∂(12) %2n! ← qif n equal 0 qthen 1 qelse n . (n - 1)!%1

which is the well known recursive program for the factorial function.
We will use capitalized italic names for programs themselves regarded
as texts and the corresponding name initialized with lower case as a
name for the function computed by the program, except that as in the
case of ⊗Factorial, we sometimes use an infix or other conventional
notation for the function.
Mutually recursive sets of function programs will also be considered.

	Another example is the Lisp program %2Append%1.  In this
paper we will use the Lisp external or publication notation of
(McCarthy and Talcott 1979), and we will write %2u*v%1 for %2append[u,v]%1.
We then have

%2Append:∂(12) %2u * v ← qif qn u qthen v qelse qa u . [qd u * v]%1.

Here we are using qn for ⊗null, qa for ⊗car, qd for ⊗cdr and an
infixed . for ⊗cons.  We omit brackets for functions of one argument.
In a more traditional Lisp M-expression notation we would have

	%2append[u,v] ← qif null[u] qthen v qelse cons[car[u], append[cdr[u], v]]%1,

and in Maclisp S-expression notation, this would be

.begin nofill

∂(8)(DEFUN APPEND (U V) 
∂(12)(COND ((NULL U) V) (T (CONS (CAR U) (APPEND (CDR U) V))))).
.end

	Our objective is to prove facts about such recursively defined
functions by regarding the recursive function definitions as sentences
of first order logic.  More accurately, we represent the recursive
function definitions by very similar sentences of first order logic.
⊗Factorial and ⊗Append are translated into the sentences

!!g5:	%2(∀n)(iseint n ⊃ n! = qif n equal 0 qthen 1 qelse n %8x%* (n - 1)!)%1

and

!!g6:	%2(∀u v)(iselist u ∧ iselist v ⊃ u * v = qif qn u qthen v qelse qa u . [qd u * v])%1

respectively.  The form of conditional expression %2qif p qthen a qelse b%1 used
in these sentences is just a function that could as well be written
⊗if(p,a,b) so far as the logic is concerned.

	The predicates ⊗iseint and ⊗iselist respectively restrict their arguments
to be extended integers (i.e. the integers extended by qb) and extended
lists.  When these domains can be taken for granted, we can omit the
explicit restrictions and write

!!g5a:	%2(∀n)(n! = qif n equal 0 qthen 1 qelse n %8x%* (n - 1)!)%1

and

!!g6a:	%2(∀u v)(u * v = qif qn u qthen v qelse qa u . [qd u * v])%1

	The sentences ({eq g5}) and ({eq g6}) completely characterize
the functions defined by the programs ⊗Factorial and ⊗Append, so proofs
of the properties of these functions can be deduced from these sentences
together with axioms characterizing the natural number and Lisp data
domains respectively.  For example, suppose we wish to prove that *
satisfies the equations

!!g7:	%2(∀v)(qNIL * v = v)%1

and

!!g8:	%2(∀u)(u * qNIL = u)%1,

i.e. qNIL is both a left and right identity for the * operation.  ({eq g7})
is trivially obtained by substituting qNIL for ⊗u in ({eq g5}) and
using the rules for evaluating conditional expressions which will have
been added to the usual rules for first order logic.  ({eq g8}) expresses a
more typical program property in that its proof requires a mathematical
induction.

This induction is accomplished by substituting

!!g9:	%2qF(u) ≡ (u * qNIL = u)%1

in the list induction schema

!!g10:	%2qF(qNIL) ∧ (∀u)(islist u ∧ ¬null u ∧ qF(qd u) ⊃ qF(u)) ⊃ (∀u)(islist u ⊃ qF(u))%1,

and using ({eq g6}), the axioms for lists, and the rules of inference
of first order logic including those for conditional expressions.

	Once the formalism has been established, totality can be proved
in the same way as other properties of the programs.  Thus the totality
of ⊗u*v is proved by substituting

!!g11:	%2qF(u) ≡ islist[u*v]%1

into the schema ({eq g10}) and using ({eq g6}), etc. as described above.

	The translation of the program into a logical sentences would
be trivial to justify if we were always assured that the program
terminates for all sets of arguments and thus
defines a total function.  The innovation is that the
translation is possible even without that guarantee at the cheap price of
extending the data domain by an undefined element qb, rewriting
recursively defined predicate programs as function programs, having two kinds of
equality and conditional expression, and providing each predicate with
two forms - one a genuine predicate in the logic
and the other a function imitating the partial predicate by a function
that takes the value qb when the program for the predicate doesn't terminate.
Proofs of termination then take the same form as other
inductive proofs.  However, additional formalism is required to characterize
completely programs that don't always terminate.

	The next sections introduce the logical basis of the formalism
and axioms and axiom schemata for Lisp.
.skip 2
.bb "#. Two Useful Extensions to First Order Logic."

	We begin by extending first order logic to include conditional
expressions and first order lambda expressions.  This allows us to
parallel the structure of recursive programs within logical sentences.

	We cannot add arbitrary programming
constructions to first order logic without risking its useful properties
such as completeness or even consistency.  Fortunately, these extensions
are harmless, because they are not merely conservative;
they can even be eliminated from wffs,
and they are generally useful.  In fact, they are useful for expressing
mathematical ideas concisely and understandably quite apart from
applications to computer science.  The reader is assumed to know about
first order logic, conditional expressions and lambda expressions; we
explain only their connection.

	Remember that the syntax of first order logic is given in the
form of inductive rules for the formation of terms and wffs.  The
rule for forming terms is extended as follows:

	If ⊗P is a wff and ⊗a and ⊗b are terms, then %2IF P THEN a ELSE b%1
is a term.  Sometimes parentheses must be added to insure unique decomposition.
Note that this makes the definitions of term and wff mutually recursive.

	The semantics of conditional expression terms is given by a rule for
determining their values.  Namely, if ⊗P is true, then the value of
%2IF P THEN a ELSE b%1 is the value of ⊗a.  Otherwise it is the value
of ⊗b. 

	It is also necessary to add rules of inference to the logic concerned
with conditional expressions.  One could get by with rules permitting
the elimination of conditional expressions from sentences and their
introduction.  These rules are important anyway, because they permit
proof of the metatheorem that the main properties of first order logic
are unaffected by the addition of conditional expressions.  These include
completeness, the deduction theorem, and semi-decidability.

	In order to state these rules it is convenient to introduce
conditional expressions also as a ternary logical connective.  A more
fastidious exposition would use a different notation for logical
conditional expressions, but we will use them so little that we might as
well use the same notation, especially since it is not ambiguous.  Namely,
if ⊗P, ⊗Q, and ⊗R are wffs, then so is %2IF P THEN Q ELSE R%1.  Its
semantics is given by considering it as a synonym for %2((P ∧ Q) ∨ (¬P ∧
R))%1.  Elimination of conditional expressions is made possible by the
distributive laws

!!z1:	%2f(IF P THEN a ELSE b) = IF P THEN f(a) ELSE f(b)%1

and
.begin nofill

!!z2: ∂(8)%2qF(IF P THEN a ELSE b) ∂(32) ≡ IF P THEN qF(a) ELSE qF(b)%1
∂(32) ≡ %2(P ∧ qF(a)) ∨ (¬P ∧ qF(b))%1
.end

where ⊗f and qF stand for arbitrary function and predicate symbols
respectively.

	Notice that this addition to the logic has nothing to do with
partial functions or the element qb.

	While the above rules are sufficient to preserve the completeness
of first order logic, proofs are often greatly shortened by using the
additional rules introduced in (McCarthy 1963).  We mention especially an
extended form of the rule for replacing an expression by another
expression proved equal to it.  Suppose we want to replace the expression
⊗c by an expression ⊗c' within the conditional expression %2IF P THEN a
ELSE b%1.  To replace an occurrence of ⊗c within ⊗a, we need
not prove %2c_=_c'%1 but merely %2P_⊃_c_=_c'%1.  Likewise if we want to
replace an occurrence of ⊗c in ⊗b, we need only prove %2¬P_⊃_c_=_c'%1.
This principle is further extended in the afore-mentioned paper.

	A further useful and eliminable extension to the logic is to allow
"first order" lambda expressions as function and predicate expressions.
Thus if ⊗x is an individual variable, ⊗e is a term, and ⊗P is a wff, then
%2(λx)e%1 and %2(λx)P%1 may be used wherever a function symbol or predicate
symbol respectively are allowed.  Formally, this requires that the
syntactic categories of <function symbol> and <predicate symbol> be
generalized to <function expression> and <predicate expression>
respectively and that these categories are then defined mutually
recursively with terms and wffs.

	The only inference rule required is lambda
conversion which serves to eliminate or introduce lambda expressions.
According to this rule, a wff is equivalent to a wff obtained
from it by replacing a sub-wff or sub-term by one obtained from
it by lambda conversion.
The rules for lambda conversion must include alphabetic changes of
bound variables when needed to avoid capture of the free variables in
arguments of lambda expressions.

	The use of minimization schemata and schemata of induction is
facilitated by first order lambda expressions, since the substitution just
replaces occurrences of the function variable in the schema by a lambda
expression which can subsequently be expanded by lambda conversion.
Using lambda expressions somewhat simplifies the rule for substitution
in schemata.  First order lambda expressions also permit many
sentences to be expressed more compactly and may be used to
avoid duplicate computations in recursive programs.  Thus we can write
%2[(λx)(x↑2_+_x)](a_+_b)%1 instead of %2(a_+_b)↑2_+_(a_+_b)%1.  Since all
occurrences of first order lambda expressions can be eliminated from wffs
by lambda conversion, the metatheorems of first order logic are again
preserved.  The reason we don't get the full lambda calculus is that the
syntactic rules of first order logic prevent a variable from being used in
both term and function positions.  While we have illustrated the use of
lambda expressions with single variable λ's, expressions like %2(λx_y_z)e%1
are also useful and give no trouble.  It is also easily seen that lambda
conversion within a term preserves its value, and lambda conversion
within a wff preserves its truth value.

	Actually it seems that even higher order λ's won't get us out of
first order logic provided rules of typing are obeyed and we provide no
way of quantifying over function variables.  Any occurrences of higher
order lambda expressions in wffs are eliminable just by carrying out the
indicated lambda conversions.  For example, we could define

	%2transitive = (λR)((∀X Y Z)(R(X,Y) ∧ R(Y,Z) ⊃ R(X,Z)))%1,

and any use of ⊗transitive in a wff would be eliminable using its
definition and lambda conversion.
.skip 2
.bb "#. Partial Functions and Partial Predicates."

	The main difficulty to be overcome in representing recursive
programs by logical sentences is that the computation of an arbitrary
recursive program cannot be guaranteed to terminate.
Consider the recursive program

%2Runaway:∂(12)%2f(n) ← f(n) + 1%1

over the integers.  If we translate ⊗Runaway into the sentence

!!q2:	%2(∀n)(f(n) = f(n) +1)%1

and use the axioms of arithmetic, we get a contradiction.

	The way out is to adjoin to our data domains an additional element
qb (read "bottom"), which is taken to be the value of the function when
the computation doesn't terminate.  In addition we add the axiom

!!q2a:	%2(∀n)(isint(n) ∨ n = qb)%1,

and modify the axioms for arithmetic to refer to elements satisfying %2isint%1.
Then going from ⊗Runaway to ({eq q2})
doesn't lead to a contradiction but to the desired result that

!!q3:	%2(∀n)(f(n) = qb)%1,

provided we also postulate that

!!q4:	%2(∀n)(n + qb = qb + n = qb)%1,

which is reasonable given the interpretation of qb as the value of
a computation that doesn't terminate.   We will postulate that all
of the base functions, except the conditional expression, have qb as
value if any argument is qb.  Such functions are called %2strict%1.
Manna (1974) calls them %2natural extensions%1 of the functions defined
on the domain without qb.

	We have discussed treating partial functions by introducing
qb.  A function takes the value qb when the program that computes it
doesn't terminate, and it is sometimes convenient to give a function
the value qb in some other cases when we want it to be undefined.

	It is convenient to introduce a rather trivial partial ordering
relation on our data domain once it has been extended by adjoining
qb.  Namely, we define the relation %2X_q<_Y%1 by

!!q5:	%2(∀X Y)(X q< Y ≡ X = qb ∧ Y ≠ qb)%1.

(Readers of (Manna 1974) should note that the symbol ≡ is being used
in its common logical sense of "if and only if").  We also
make corresponding definitions of q>, q≤, and q≥.  The ordering
can be extended to functions by defining

!!q6:	%2f q≤ g ≡ (∀X)(f(X) q≤ g(X))%1.

This induced ordering is not so trivial, but we don't use it in this
paper, since it gets us out of first order logic.  Even though ({eq q5})
defines a rather trivial ordering, we find that it shortens and
clarifies many formulas.

	Partial predicates give rise to new problems.  The computation of
a recursively defined predicate may not terminate, so the same problem
arises.  However, we can't solve it in the same way without adding an
additional undefined truth value to the logic.  This would give rise to a
partial first order logic in which sentences could be true, false or
undefined.  Various partial predicate calculi have been studied in
(McCarthy 1964), (Bochvar 1938 and 1943) and elsewhere,
but they have the serious disadvantage that
arguments by cases become quite long, since three cases always have to be
provided for, even when most of the predicates are known to be total.
Moreover, existing logic texts, proof-checkers and theorem provers all use
total logic.  Therefore, it seems better to keep the logic conventional
and handle partial predicates as functions.

	We introduce a domain %AP%1 with three elements ⊗T, ⊗F and qb
called the domain of extended truth values.  In a sorted logic, this may
be a separate sort.  Otherwise, it may be considered either separately or
as part of the main data domain.  In Lisp it is convenient to regard ⊗T 
and ⊗F as special atoms and to use the same qb for extended truth values
as for extended S-expressions.  It is even possible to follow the Lisp
implementations that use qNIL for ⊗F and interpret all other S-expressions
as ⊗T, although we don't do that in this paper.

	It is convenient to define first a form of conditional
expression that takes an extended truth value as its first argument,
namely

	%2qif p qthen a qelse b = IF p = qb THEN qb ELSE IF p = T THEN a ELSE b%1.

The only difference between then extended conditional expression and
the logical conditional expression is that since the extended
conditional expression takes an extended truth value as propositional
argument, we can provide for the possibility that the computation
of that argument fails to terminate.  Since the extended conditional
expression treats the undefined cases according to their behavior in
programs, we use the same notation as previously used for programs.

	Extended boolean operators are conveniently defined using the
extended conditional expressions.  For every predicate or boolean
operator, we introduce a corresponding function taking extended truth
values as operands and taking an extended truth value as its value.  Thus
the function ⊗and, is written with an infix and defined by

	%2p and q = qif p qthen q qelse F%1

The function ⊗and is distinct from the logical operator ∧ which remains
in the logic.  To illustrate this, we have the true sentence

	%2((p and q) = T) ≡ (p = T) ∧ (q = T)%1.

The parentheses in the above can be omitted without ambiguity
given suitable precedence rules.  Note that ⊗and has the
non-commutative property of (McCarthy 1963), namely %2F_and_qb_=_F%1
while %2qb_and_F_=_qb%1.  This corresponds to the fact that
it is convenient to compute %2p_and_q%1 by a program that doesn't
look at ⊗q if ⊗p is false but which doesn't terminate if the
computation of ⊗p doesn't terminate.  Symmetry could be restored
if the computer time-shared its computations of ⊗p and ⊗q, but
there are too many practical disadvantages to such a system to
justify doing it for the sake of mathematical symmetry.  Algol 60
requires that both ⊗p and ⊗q be computed which precludes using
boolean opeators as the main connectives of Lisp type recursive
definitions of predicates.

	Other extended boolean operators are defined by

	%2p or q = qif p qthen T qelse q%1

and

	%2not p = qif p qthen F qelse T%1.

	We also require an equality function that extends logical equality,
namely

	%2X equal Y = IF X = qb ∨ Y = qb THEN qb ELSE IF X = Y THEN T ELSE F%1.

	Readers familiar with (Manna 1974) should note that we write = where
Manna writes ≡, and we write ⊗equal where Manna writes =.  We have chosen
our notation to conform to that of first order logic with equality.

	In fact, the key to successful representation of recursive programs
in first order logic is the simultaneous use of true equality in the logic
in order to make assertions freely and the ⊗equal function that gives an
undefined result for undefined arguments.  The latter describes the behavior
of an equality test within the program.  The two forms of conditional
expression are also essential.

	The partial ordering q< is also useful applied to extended
truth values.

	We summarize this in the following set of axioms:

T1:	%2(∀p)(istv p ≡ p = T ∨ p = F)%1

T2:	%2(∀p)(isetv p ≡ istv p ∨ p = qb)%1

T3:	%2T ≠ F ∧ ¬istv qb%1

.begin nofill

T4: %2(∀p X Y)(isetv p ⊃ 
∂(12)qif p qthen X qelse Y = IF p = qb THEN qb ELSE IF p = T THEN X ELSE Y)%1
.end

T5:	%2(∀p)(isetv p ⊃ not p = qif p qthen F qelse T)%1

T6:	%2(∀p q)(isetv p ∧ isetv q ⊃ p and q = qif p qthen q qelse F)%1

T7:	%2(∀p q)(isetv p ∧ isetv q ⊃ p or q = qif p qthen T qelse q)%1

T8:	%2(∀X Y)(X equal Y = IF X = qb ∨ Y = qb THEN qb ELSE IF X = Y THEN T ELSE F%1

T9:	%2(∀p)(isetv p ∧ isetv q ⊃ (p q< q ≡ p = qb ∧ (q = T ∨ q = F)))%1.
.skip 2
.bb "#. The Functional Equation of a Recursive Program - Theory."

	The familiar recursive program

!!d1:	%2u * v ← qif qn u qthen v qelse qa u . [qd u * v]%1

is a special case of a system of mutually recursive programs
which can be written

.begin nofill
.turn on "[]"

!!d2:	∂8%2f↓1(x↓1,...,x↓[m↓1]) ← qt↓1(f↓1, ... ,f↓n,x↓1, ... ,x↓[m↓1])%1
	∂8.
	∂8.
	∂8.
	∂8%2f↓n(x↓1,...,x↓[m↓n]) ← qt↓n(f↓1, ... ,f↓n,x↓1, ... ,x↓[m↓n])%1.
.end

Here the qt's are terms in the individual variables %2x↓1%1, etc. and the
function symbols %2f↓1,_..._f↓n%1.  All the essential features of such
mutual recursive definitions arise when there is only one function, but
phenomena arise when there are two or more arguments to the functions that
do not arise in the one argument case - two arguments being sufficiently
general.  Therefore, we write

!!d2a:	%2f(x,y) ← qt(f,x,y)%1,

which may also be written

!!d2b:	%2f(x,y) ← qt[f](x,y)%1

when we wish to emphasize that qt maps a partial function ⊗f into another
partial function %2qt[f]%1.

	In this paper, we shall mainly consider recursive programs over
S-expressions, lists and integers, but we can actually start with an
arbitrary collection of base functions and predicates
over a collection of domains and define the functions %2computable in
terms of the base functions%1.  This is discussed in (McCarthy 1963).
In a discussion of the basic ideas, full generality is superfluous,
and all the interesting phenomena arise with a single domain - call
it ⊗D, extended to %2D↑+%1 by adjoining qb and with characteristic
predicate ⊗isD. 

	Such a program or system of mutually recursive programs can be
regarded as defining a partial function in several ways.

1. It can be compiled into a machine language program for some
computer using call-by-value.  The resulting program is a subroutine
that calls itself recursively.  Before it is called, the values
of the arguments must be computed and stored in suitable conventional
registers.  This includes its calls to itself.  Most Lisp implementations
as well as most implementations of other programming languages use
call-by-value.

2. It can be compiled into a machine language program for some
computer using call-by-name.  The resulting program again calls
itself recursively.  It is called by storing into suitable registers
the location of programs for computing the expressions that have
been written as its arguments.  Thus %2((w.z)*f(u))%1  would be
compiled into program that would give the program for ⊗u*v pointers
to program for computing ⊗w.z and ⊗f(u).  The program for * could
call these other programs whenever it wanted its arguments.  In
the case of ⊗u*v, there is nothing the program can profitably do
except call for both of its arguments.  However, a program for
multiplying two matrices might call its first argument, and, if
the first argument turned out to be the zero matrix, not bother
to call the second argument.

	We can also consider evaluating the function by symbolic computation.
Namely, we substitute the arguments of the function * for ⊗u and ⊗v, and
then evaluate the right hand side of the definition.  There are many
ways to do this evaluation, because there may be more than one occurrence
of the function being defined on the right hand side of the definition,
but two of them correspond to call-by-name and call-by-value respectively.

3. When evaluating a conditional expression, always evaluate the
propositional term first and use it to decide which of the other terms to
evaluate first.  When evaluating a term formed by composition of
functions, if there is only one occurrence of the function being defined
on the right hand side, there is no choice to be made, but if there is
more than one, expand the leftmost innermost first.  If it gives an answer
substitute it and continue the process.  If it gives further recursion,
then proceed with its leftmost innermost, etc.
This corresponds to call-by value.

4. If instead of expanding the leftmost innermost occurrence of the
function first, we expand the outermost occurrences, we get an evaluation
method corresponding to call-by-name.

	It should also be proved that evaluation by substitution and
evaluation by subroutine both using call-by-value give the same results.
The two ways of doing call-by-name should also be proved to
give the same results.  Such a proof would involve reasoning about the
operation of subroutine calls and the saving of temporary storage
registers on the stack.  We are not aware of a published proof of
these statements or even a precise statement of them.

	Computing ⊗u*v doesn't show the difference between these
methods, but consider the function

!!d3:	%2morris(x,y) ← qif x equal 0 qthen 0 qelse morris(x - 1, morris(x, y))%1

introduced in (Morris 1968).
Evaluating ⊗morris(2,1) by either call-by-value method leads to an
infinite computation, because the term ⊗morris(x,_y) has to be
evaluated all over.  Call-by-name
evaluation, on the other hand, gives the answer 0, because the second
argument of ⊗morris is never called.
Vuillemin (1973) shows that
whenever call-by-value gives an answer, call-by-name gives
the same answer, but sometimes call-by-name gives an answer when
call-by-value doesn't.  If we force a program to be ⊗strict, i.e.
to demand that all of its arguments are defined, then call-by-name
and call-by-value are equi-terminating - to coin a word.

	(Manna 1974) also contains proofs of these assertions.

	Execution of recursive programs by substitution 
is inefficient, but provides a good theoretical tool for classifying
the more efficient subroutine methods of evaluation.

5. Finally, we can regard ({eq d1}) and ({eq d3}) as functional
equations for * and ⊗morris respectively.  In general, a
functional equation may have many solutions or none.
However, it is essentially Kleene's (1952) first recursion theorem,
(see Manna 1974, theorem 5-2) that if the right
side is %2continuous%1 in the function being defined and in the
individual variables, there will be a unique %2minimal%1 solution.
This condition is assured if the right hand side is a term built from
strict functions and predicates by composition and the formation
of extended conditional expressions.  Continuity is discussed in (Manna 1974).
It is not permitted to use logical conditional expressions without
satisfying additional hypotheses, and this
restriction prevents true equality or any predicate from direct use.
If logical conditional expressions were generally allowed, we could have
sentences like

!!d3a:	%2(∀x)(f(x) = IF f(x) = qb THEN T ELSE qb)%1

which are self-contradictory.  The corresponding version using extended
conditional expressions, namely

!!d3b:	%2(∀x)(f(x) = qif f(x) equal qb qthen T qelse qb)%1

is satisfied by %2f(x) = qb%1 and is therefore harmless.
Logical conditional expressions can be used when
we can guarantee that the propositional part is total and in some other cases.

	The
minimal solution is minimal in the sense that any other solution
is greater in the ordering of functions previously given, i.e. if
⊗f is the minimal solution and qf is another solution, then

!!d4:	%2(∀x y)(f(x,y) q≤ qf(x,y))%1.

	The minimal solution of the functional equation
can therefore be characterized by the schema

!!d5:	%2(∀x y)(qf(x,y) = qt[qf](x,y)) ⊃ (∀x y)(f(x,y) q≤ qf(x,y))%1.
.skip 2
.bb "#. Axioms for S-expressions, Lists and Integers."
.turn on "↓"

	The collection of axioms Lisp1 allows for the possibility that
there are other kinds of entity besides S-expressions, lists and integers.
In practical program proving, these will include sets and data structures
of various kinds.  In consequence of this decision, we need the predicates
⊗issexp, ⊗islist and ⊗isint to pick out S-expressions, lists and integers
respectively.  Lists are considered to be a particular kind of
S-expression, namely S-expressions such that going in the ⊗cdr direction
eventually reaches qNIL.  It is convenient to have both the predicates
⊗atom and ⊗ispair that pick out atomic and non-atomic S-expressions
respectively.

	Lisp1 is convenient for making proofs and is intended
to treat S-expressions, lists and integers as similarly as possible.
Therefore, the axioms are highly redundant.  Adjoining qb to the domains has
both conveniences and inconveniences.  The main convenience is that the
recursive definitions now give total functions.  A major inconvenience
is that algebraic relations often require qualification, e.g. %20 qx_x_=_0%1
isn't true if %2x_=_qb%1.

	Our first axiom gives the algebraic relations of ⊗cons, ⊗car and ⊗cdr. 

S1:	%2(∀x y)(issexp x ∧ issexp y ⊃ ispair[x.y] ∧ qa[x.y] = x ∧ qd[x.y] = y)%1

	The definition of atoms and pairs:

S2:	%2(∀x)((ispair x ≡ issexp x ∧ ¬atom x) ∧ (atom x ⊃ issexp x))%1

	Taking apart an S-expression and putting the parts back together
gives back the original expression.

S3:	%2(∀x)(ispair x ⊃ issexp qa x ∧ issexp qd x ∧ x = qa x . qd x)%1

	Lists are included among S-expressions.

S4:	%2(∀u)(islist u ⊃ issexp u)%1

	%2cons%1ing an S-expression onto a list gives a list.

S5:	%2(∀x u)(issexp x ∧ islist u ⊃ islist[x.u])%1

	qNIL is the only atomic list and only qNIL satisfies the predicate ⊗null. 

S6:	%2(∀u)((islist u ∧ atom u ≡ u = qNIL) ∧ (null u ≡ u = qNIL))%1

	The simple structural induction schema for S-expressions:

S7:	%2(∀x)(atom x ⊃ qF x) ∧ (∀x)(ispair x ∧ qF qa x ∧ qF qd x ⊃ qF x) ⊃ (∀x)(issexp x ⊃ qF x)%1

	The simple structural induction schema for lists:

S8:	%2qF qNIL ∧ (∀u)(islist u ∧ ¬null u ∧ qF qd u ⊃ qF u) ⊃ (∀u)(islist u ⊃ qF u)%1

	%2x ≤↓S y%1 means that ⊗x is a subexpression of ⊗y and is a
well-founded partial ordering.  It is important
for course-of-values induction for S-expressions.

S9:	%2(∀x y)(issexp x ∧ issexp y ⊃ x ≤↓S y ≡ x = y ∨ ¬atom y ∧ (x ≤↓S qa y ∨ x ≤↓S qd y))%1

	Definition of proper subexpression:

S10:	%2(∀x y)(x <↓S y ≡ x ≤↓S y ∧ x ≠ y)%1

	The course-of-values structural induction schema for S-expressions:

S11:	%2(∀x)(issexp x ∧ (∀y)(issexp y ∧ y <↓S x ⊃ qF y) ⊃ qF x) ⊃ (∀x)(issexp x ⊃ qF x)%1

	%2u ≤↓L v%1 is the natural well-founded partial ordering for lists.
It can be read "The list %2u%1 is a tail of the list %2v%1".

S12:	%2(∀u v)(islist u ∧ islist v ⊃ u ≤↓L v ≡ u = v ∨ ¬null v ∧ u ≤↓L qd v)%1

	⊗u is a proper tail of ⊗v. 

S13:	%2(∀u v)(u <↓L v ≡ u ≤↓L v ∧ u ≠ v)%1

	The course-of-values induction schema for lists.  Course-of-values
induction schemata are all the same except for the ordering used.

S14:	%2(∀u)(islist u ∧ (∀v)(islist v ∧ v <↓L u ⊃ qF v) ⊃ qF u) ⊃ (∀u)(islist u ⊃ qF u)%1

	These axioms for integers are based on the successor and predecessor
functions and are analogous to the above axioms for S-expressions.  They
are equivalent to the usual first order number theory.

	The relation between the successor and predecessor functions:

I1:	%2(∀n)(isint n ⊃ isint succ n ∧ succ n ≠ 0 ∧ pred succ n = n)%1

	As a function in the logic, the predecessor must always have a
value.  However we say something about %2pred_n%1 only for non-zero ⊗n. 

I2:	%2(∀n)(isint n ∧ n ≠ 0 ⊃ isint pred n ∧ succ pred n = n)%1

	The simple induction schema for integers:

I3:	%2(qF 0 ∧ (∀n)(isint n ∧ n ≠ 0 ∧ qF pred n ⊃ qF n) ⊃ (∀ n)(isint n ⊃ qF n)%1

	For course-of-values induction, we need the ordering relations.

I4:	%2(∀m n)(isint m ∧ isint n ⊃ (m ≤ n ≡ m = n ∨ n ≠ 0 ∧ m ≤ pred n))%1

	Proper ordering:

I5:	%2(∀m n)(m < n ≡ m ≤ n ∧ m ≠ n)%1

	The course-of-values schema:

I6:	%2(∀n)(isint n ∧ (∀m)(isint m ∧ m < n ⊃ qF m) ⊃ qF n) ⊃ (∀n)(isint n ⊃ qF n)%1

	The recursive definition of addition:

I7:	%2(∀m n)(isint m ∧ isint n ⊃ m + n = IF n = 0 THEN m ELSE succ m + pred n)%1

	Multiplication:

I8:	%2(∀m n)(isint m ∧ isint n ⊃ m qx n = IF n = 0 THEN 0 ELSE m + m qx pred n)%1

	The next group of axioms are concerned with extending the domain by
adjoining qb.  The predicates of the extended domains are ⊗isesexp, ⊗iselist 
and ⊗iseint respectively.

	Extending the S-expressions with qb:

E1:	%2(∀x)(isesexp x ≡ issexp x ∨ x = qb)%1

	Extending the lists with qb:

E2:	%2(∀u)(iselist u ≡ islist u ∨ u = qb)%1

	Extending the integers with qb:

E3:	%2(∀n)(iseint n ≡ isint n ∨ n = qb)%1

	We need a function taking the value T when its argument is an
S-expression.  It will be used in extended conditional expressions.

E4:	%2(∀x)(issexpf x = IF x = qb THEN qb ELSE IF issexp x THEN T ELSE F)%1

	Likewise for lists:

E5:	%2(∀u)(islistf u = IF u = qb THEN qb ELSE IF islist x THEN T ELSE F)%1

	Likewise for integers:

E6:	%2(∀n)(isintf n = IF n = qb THEN qb ELSE IF isint x THEN T ELSE F)%1

	Extending the integer functions to take qb as an argument.  The
extension is ⊗strict, i.e. the extended values are all qb.

E7:	%2succ qb = qb ∧ pred qb = qb%1

	Extending the Lisp functions strictly to take qb as an argument:

E8:	%2qa qb = qb ∧ qd qb = qb%1

	The strict extension of ⊗cons.  (Friedman and Wise (1977) propose
a non-strict extension).

E9:	%2(∀x)(x.qb = qb ∧ qb.x = qb)%1

	The functions qat and qn are defined from the predicates ⊗atom 
and ⊗null. 

E10:	%2(∀x)(qat x = IF x = qb THEN qb ELSE IF atom x THEN T ELSE F)%1

E11:	%2(∀u)(qn u = IF u = qb THEN qb ELSE IF null u THEN T ELSE F)%1
.skip 2
.bb "#. Forms of Induction."

	All proofs of non-trivial program properties require some form
of mathematical induction.  Methods of induction can be divided into
three classes - induction on data, various forms of computation induction
on approximations to the program, and induction on the course of the
computation.  It is not certain that that these are really distinct; i.e.
there may be systematic ways of regarding one as a form of another.
In this section, we deal only with induction on data.

	Induction on data often takes a form called
structural induction in which the data domain consists of objects
built up from elementary objects by a fixed finite set of operations.
The construction of S-expressions from atoms by ⊗cons or the construction
of the integers from zero by the successor operation are examples.

	Induction can take two forms.  One form involves the constructors or
selectors of the domain directly.  Simple list, S-expression, and
numerical induction are examples.  The second form is a course-of-values
induction schema

!!i1:	%2(∀x)(isD x ∧ (∀y)(isD y ∧ y < x ⊃ qf y) ⊃ qf x) ⊃ (∀x)(isD x ⊃ qf x)%1

based on an ordering relation < defined in terms of the
selector functions.  Course-of-values schemata were also given for
lists, S-expression and natural numbers.  Course-of-values often gives
a proof with a simpler induction predicate than simple induction.

A simple example is the termination of the list function ⊗alt defined by

!!i2:	%2alt u ← qif qn u or qn qd u qthen u qelse qa u . alt qdd u%1.

Because of the qdd, simple induction doesn't work on the obvious predicate

!!i3:	%2qF(u) ≡ islist alt u%1,

but course-of-values induction does work.

	In the simple cases we have seen so far, the induction is on
one of the variables in the program, but this is not the general
case.  More generally, the induction is on some function of the
variables, and the domain of this function may be quite different
from that of the variables of the progam.  Often it can be taken
to be the natural numbers, but more generally it can be any partially
ordered domain in which all descending chains are finite.

	For example S-expression can be replaced by induction on 
natural numbers by introducing the function %2size_x%1 defined by

!!i3a:	%2size x ← qif qat x qthen 1 qelse size qa x + size qd x%1

Size has the property that %2size qa x < size x%1 and
%2size qd x < size x%1.  
We can prove that a formula %2qF(x)%1 holds for all S-expressions 
by "induction on the size of %2x%1".  This is done by proving that the formula
qF' given by

!!i3b:	%2qF'(n) ≡ (∀x)(size x = n ⊃ qF(x))%1

holds for all numbers using numerical induction.   In fact 
any proof of the formula qF by S-expression induction can easily be converted to
a proof of qF' by numerical induction and vice versa.


	A more exotic example of this is provided by the Takeuchi
function (Takeuchi 1978) defined by
.skip
.begin nofill;
!!i4: ∂(9)%2tak(m,n,p) ← 
∂(12)qif m lesseq n qthen n qelse tak(tak(m-1,n,p),tak(n-1,p,m),tak(p-1,m,n))%1.
.end

	The function is total when the arguments are integers and
is equal to

!!i5:	%2tak0(m1,m2,m3) = IF m1 ≤ m2 THEN m2 ELSE IF m2 ≤ m3 THEN m3 ELSE m1%1.

The most convenient proof that ⊗tak is total uses the course-of-values
schema for integers with

!!i6:	%2qF(n) ≡ (∀m1 m2 m3)(rank(m1,m2,m3) = n ⊃ tak(m1,m2,m3) = tak0(m1,m2,m3))%1,

where

!!i7:	%2rank(m1,m2,m3) = dtak1(m1-m2,m3-m2)%1,

and

.begin nofill
!!i8:	%2dtak1(n1,n2) = ∂(23)IF n1 ≤ 0 THEN 0
%2∂(23)ELSE IF n2 ≥ 2 THEN m + n(n - 1)/2 -1
%2∂(23)ELSE IF n ≥ 0 THEN m
%2∂(23)ELSE IF n = -1 THEN (m + 1)(m + 2)/2 - 1
%2∂(23)ELSE (m - n)(m - n + 1)/2 - m - 1%1.
.end

This is an example of the more general form of inductive proof.  A rank
function is defined taking values in some inductively ordered domain
(in this case the natural numbers), and the theorem is proved under the
hypothesis that it is true for all lower rank tuples of variables.
The term %2structural induction%1 seems no longer applicable to this
general case, because it is not an induction on the structure of the
data domain of the program, although it requires no new machinery when
we are operating within first order logic.  Perhaps %2structural induction%1
was a misnomer anyway, since the more general form corresponds to how
mathematicians already looked at induction.

	The inductively ordered set serving as the domain of the rank
function is chosen for convenience, where the object is to get a short
and understandable proof.  If we only care about whether a proof exists
and not how easy it is to write and read, then all the domains considered
so far are equivalent to the natural numbers.  To get something stronger,
we go to induction over transfinite ordinal numbers
- explained in most books on axiomatic set theory.

.begin turn on "[]"
	The axiom schema for induction over ordinals is just the usual
course-of-values schema written with the ordering over the ordinals,
say ≤↓o.  In order to use it, this ordering must be defined, and we
must be able to write a rank function from tuplets to ordinals.  This
requires that we use a notation for ordinals, and any given notation
represents only the ordinals less than some bound.  Most proofs arising
in practice will involve only ordinals less than qw↑[qw] which can be
represented as polynomials in qw.
.end

	An example requiring induction up to qw↑2 is proving the termination
of Ackermann's function which has the functional equation 
.skip
.begin nofill
!!i9: ∂(8)%2(∀m n)(A(m,n) = 
∂(15)qif m equal 0 qthen n+1 qelse qif n equal 0 qthen A(m-1,0) qelse A(m-1,A(m,n-1)))%1.
.end

The statement to be proved is

!!i10:	%2(∀αα)(αα < qw↑2 ⊃ qF(αα))%1,

where	

!!i11:	%2(∀αα)(qF(αα) ≡ (∀m n)(rank(m,n) = αα ⊃ isint A(m,n)))%1,

and

!!i11a:	%2(∀m n)(rank(m,n) = qwm + n)%1.

The proof is straightforward, because %2qw(m-1) < qwm+n%1 and %2qwm+(n-1) < qwm+n%1,
so we can assume %2isint A(m-1,0)%1 and %2isint A(m,n-1)%1.  From the latter,
it follws that %2qw(m-1)+A(m,n-1)%1 < qwm+n%1 which completes the induction
step.
	
.skip 2
.bb "#. An Extended Example."

	The SAMEFRINGE problem is to write a program that efficiently
determines whether two S-expressions have the same fringe, i.e. have
the same atoms in the same order.  (Some people omit the qnils at the ends
of lists, but we will take all atoms).  Thus
((A.B).C) and (A.(B.C)) have the same fringe, namely (A B C).  The
object of the original problem was to program it using a minimum of 
storage, and it was conjectured that co-routines were necessary to
do it neatly.  We shall not discuss that matter here - merely the
extensional correctness of one proposed solution.

	The relevant recursive definitions are

!!n1:	%2fringe x ← qif qat x qthen <x> qelse fringe qa x * fringe qd x%1,

We are interested in the condition %2fringe x = fringe y%1.

	The function to be proved correct is %2samefringe[x,y]%1 defined by
the simultaneous recursion

!!n3:	%2samefringe[x, y] ← (x equal y) or [not qat x and not qat y and same[gopher x, gopher y]]%1,

!!n4:	%2same[x, y] ← (qa x equal qa y) and samefringe[qd x, qd y]%1,

where

!!n5:	%2gopher x ←  qif qat qa x qthen x qelse gopher qaa x . [qda x . qd x]%1.

	We need to prove that %2samefringe%1 is total and

!!n6:	%2(∀xy)(samefringe[x,y] = T ≡ fringe x = fringe y)%1.

The functional equations are

!!n7:	%2(∀x)(fringe x = qif qat x qthen <x> qelse fringe qa x * fringe qd x%1),

!!n8:	%2(∀u v)(u * v = qif qn u qthen v qelse qa u . [qd u * v])%1.
.begin nofill

!!n9: ∂(8)%2(∀x y)(samefringe[x, y] = 
∂(16)x equal y or [not aat x and not aat y and same[gopher x, gopher y]])%1,
.end

!!n10:	%2(∀x y)(same[x, y] = qa x equal qa y and samefringe[qd x, qd y]%1,

!!n11:	%2(∀x)(gopher x =  qif qat qa x qthen u qelse gopher qaa x . [qda x . qd x])%1.

	We shall not give full proofs but merely the induction predicates
and a few indications of the algebraic transformations.  We begin with
a lemma about %2gopher%1.

!!n12:	%2(∀x y)(ispair gopher[x.y] ∧ atom qa gopher[x.y] ∧
fringe gopher[x.y] = fringe[x.y])%1.

	This lemma can be proved by S-expression structural induction on %2x%*
using the predicate

!!n13:	%2qF(x) ≡ (∀y)(ispair gopher[x.y] ∧ atom qa gopher[x.y] ∧ fringe gopher[x.y] = fringe[x.y])%1.

In the course of the proof, we use the associativity of * and the
formula %2fringe[x.y]_=_fringe_x_*_fringe_y%1.
The lemma was expressed using %2gopher[x.y]%1 in order to avoid
considering atomic arguments for %2gopher%1, but it could have
equally well be proved about %2gopher_x%1 with the condition
%2¬atom_x%1.


	For our proof about %2samefringe%1 we need one more lemma
about %2gopher%1, namely

!!n16:	%2(∀x y)(size gopher[x.y] = size[x.y]%1.

	This can be proved by S-expression induction on %2x%1 separately
or as a part of the above lemma by including %2size_gopher[x.y]_=_size[x.y]%1 
as a conjunct in ({eq n12}) and ({eq n13}).

	The statement about ⊗samefringe is

!!n17:	%2(∀x y)(issexp samefringe[x,y] ∧ samefringe[x,y] = T ≡ fringe x =
fringe y)%1,

and it is most easily proved by induction on %2size_x_+_size_y%1 using
the predicate 
.skip
.begin nofill
!!n18: ∂(8)%2qF(n) ≡ (∀x y)(n = size x + size y ⊃
∂(20)issexp samefringe[x,y] ∧ (samefringe[x,y] = T ≡ fringe x = fringe y))%1.
.end

It can also be proved using the well-foundedness of lexicographic ordering
of the list %2<x, qa x>%1, but then we must decide what lexicographic orderings
to include in our axiom system.

	Transfinite induction is also useful, and can be illustrated
with a variant %2samefringe%1 that does everything in one complicated
recursive definition, namely  
.next page
.begin nofill
!!n19: ∂(8)%2samefringe[x,y] ← 
∂(12)(x equal y) or 
∂(12)not qat x and not qat y and
∂(16)qif qat qa x qthen [qif qat qa y qthen qa x equal qa y and samefringe[qd x, qd y] 
∂(28)qelse samefringe[x, qaa y . [qda y . qd y]]]
∂(16)qelse samefringe[qaa x . [qda x .qd x], y]%1.
.end

The transfinite induction predicate then has the form
.begin nofill

!!n20: ∂(8)%2qF(n) ≡ (∀x y)[n = %Aw%*(size x + size y) + size qa x + size qa y ⊃
∂(20)issexp samefringe[x,y] ∧ (samefringe[x,y] = T ≡ fringe x = fringe y)]%1.
.end

	We would like to prove that the amount of storage used in the
computation of %2samefringe[x,y]%1 aside from that occupied by ⊗x and ⊗y, 
never exceeds the sum of the numbers of %2car%1s required to reach
corresponding atoms in ⊗x and ⊗y.  Unfortunately, we can't even express
that fact, because we are axiomatizing the programs as functions,
and the amount of storage used does not depend merely on the function
being computed; it depends on the method of computation.  We may regard
such things as %2intensional%1 properties, but any correspondence with
the notion of
intensional properties in intensional logic remains to be established.
Many such intensional properties of a program are extensional properties
of certain "derived programs", and some are even extensional properties of
the functional qt.
.bb "#. The Minimization Schema."

	The functional equation of a program doesn't completely
characterize it.  For example, the program

!!h9a:	%2f1 x ← f1 x%1

leads to the sentence

!!h10:	%2(∀x)(f1 x = f1 x)%1

which provides no information although the function ⊗f1 
is undefined for all ⊗x.  This is not always the case, since
the program

!!h11:	%2f2 x ← (f2 x).qnil%1

has the functional equation

!!h12:	%2(∀x)(f2 x = (f2 x).qnil)%1.

from which %2(∀x)¬issexp f2(x)%1 can be proved by induction.

	In order to characterize recursive programs, we need some
way of asking for the least defined solution of the functional equation.

	Suppose the program is

!!h13:	%2f(x,y) ← qt[f](x,y)%1

yielding the functional equation

!!h14:	%2(∀x y)(f(x,y) = qt[f](x,y)%1.

The %2minimization schema%1 is then

!!h15b:  %2(∀x)(qt[qf](x) q≤ qf(x)) ⊃ (∀x)(f(x) q≤ qf(x))%1.

	In the case of ⊗Append we have

!!h16a:	%2(∀u v)(qf(u,v) q≥ qif qn u qthen v qelse qa u . qf(qd u, v))
⊃ (∀u v)(qf(u,v) q≥ u*v)%1.

	In the schema %Af%* is a free function variable of the appropriate
number of arguments.  The schema is just a translation into first order
logic of Park's (1970) theorem.

!!h17:	%2qf q≥ qt[qf] ⊃ qf q≥ Y[qt]%1.

Here %2Y%1 is the least fixed point operator.   

.if false then begin "hide"
The "q≥" in the hypothesis
of ({eq h15b}) and ({eq h17}) can be replaced by "=" as 
%2qf q≥ qt[qf] ≡ qf = qt[qf]%1 for continuous functionals qt.
.end "hide"

[Note that this theorem is a generalization to continuous functionals of the
second part of Kleene's first rescursion theorem (Kleene 1952)].

	The simplest application of the schema is to show that the ⊗f1 
defined by ({eq h9a}) is never an S-expression.  The schema becomes

!!h18:	%2(∀x)(qf x q≥ qf x) ⊃ (∀x)(qf x q≥ f1 x)%1,

and we take

!!h19:	%2qf x = qb%1.

The left side of ({eq h18}) is identically true, and, remembering that qb
is not an S-expression, the right side tells us that %2f1 x%1 is never
an S-expression.

	The minimization schema can sometimes be used to show partial
correctness.  For example, the well known 91-function is defined by
the recursive program over the integers

!!h20:	%2f91 x ← qif x greater 100 qthen x - 10 qelse f91 f91(x + 11)%1.

The goal is to show that

!!h22:	%2(∀x)(f91 x = IF x > 100 THEN x - 10 ELSE 91)%1.

We apply the minimization schema with

!!h21:	%2qf x ← qif x greater 100 qthen x - 10 qelse 91%1,

and it can be shown by an explicit calculation without induction that
the premiss of the schema is satisfied, and this shows that ⊗f91, 
whenever defined has the desired value.

	The method of recursion induction (McCarthy 1963) is also
an immediate application of the minimization schema.  If we show
that two functions satisfy the schema of a recursive program, we
show that they both equal the function computed by the program on
wherever the function is defined.

	The utility of the minimization schema for proving partial
correctness or non-termination depends on our ability to name
suitable comparison functions.  f1 and f91 were easily treated,
because the necessary comparison functions could be given explicitly
without recursion.  Any extension of the language that provides new
tools for naming comparison functions, e.g. going to higher order
logic, will improve our ability to use the schema in proofs.
.skip 1
.bb "#. Derived Programs and Complete Recursive Programs."

	The methods considered so far in this paper concern %2extensional%1
properties of programs, i.e. properties of the function computed by
the program.  The following are not extensional properties: the number
of times a certain function is evaluated in executing the program including
as a special case the number of recursions, the maximum depth of recursion,
and
the maximum amount of storage used.  Some of these properties depend on
whether the program is executed call-by-name or call-by-value, while others
are extensional properties of the functional of the program.

	Many of these ⊗intensional properties of a program are extensional
properties of related programs called %2derived programs%1.  For example,
the number of ⊗cons operations done by ⊗Append can be computed by a program
of the same recursive structure, namely

!!j1:	%2ncappend[u,v] ← qif qn u qthen 0 qelse 1 + ncappend[qd u, v]%1.

If we define ⊗flat by

!!j2:	%2flat[x,u] ← qif qat x qthen x.u qelse flat[qa x,flat[qd x u]]%1,

then the number of recursions done by ⊗flat is given by

!!j2a:	%2nrflat[x,u] ← qif qat x qthen 1 qelse 1 + nrflat[qa x,flat[qd x,u]]
+ nrflat[qd x,u]%1,

noticing that ⊗nrflat is mutually recursive with ⊗flat itself.  The
maximum depth of recursion of the 91-function is given by

!!j3:	%2df91 n ← 1 + qif n greater 100 qthen 0 qelse 
max(df91(n + 11),df91(f(x + 11)))%1.

	Morris (1968) discussed a derived function that gives successive
approximations of bounded recursion depth to a recursive function by modifying
the definition to take a "rationed" number of allowed recursions.  For
⊗append we would have 
.skip
.begin nofill
!!j4: ∂(8)%2append1[n,u,v] ← 
∂(12)qif n equal 0 qthen qb qelse qif qn u qthen v qelse qa u . append1[n - 1,qd u,v]%1.
.end

Thus %2append1[n,u,v]%1 computes ⊗u*v but with a ration of ⊗n recursions.  If
the computation would require more than ⊗n recursions, the value is qb, i.e.
is undefined.

	We can give a general rule for the rationed recursion function.  
Suppose that qt is a program for the function ⊗f(x,y).  

%2P:	f(x,y) ← qt[f](x,y)%1

Then

%2C(P):	g(n,x,y) ← qt'[g](n,x,y)%1

where

!!j5:	%2qt'[qf] = (λn x y)(qif n equal 0 qthen qb qelse qt[(λ x y)qf(n-1,x,y)]
(x,y))%1

is a program for the rationed recursion function ⊗g(n,x,y).  In this case,
the functional for the derived function is expressed by a formula in the
functional for the original function.  This can't always be done.

	We can use the rationed recursion function as an alternate to the
%2minimiztion schema%1 for completing the characterization of %2f%4P%1.
Namely we have

!!j5a:	%2(∀x y)(isD %2f%4P%1(x,y) ≡ (∃n)(isD %2f%4C(P)%1(x,y)))%1,

and whether %2f%4C(P)%2(x,y)%1 is defined for given arguments is determined
by its functional equation, because ⊗C(P) is what (Cartwright 1978) calls
a complete recursive program.

	A recursive program ⊗P is called complete if its functional qt%4P%1 has
only one fixed point %2f%4P%1.  Since the minimization schema is used for
distinguishing the least fixed point, it is redundant for complete
programs.  The idea of complete recursive program was first advanced in
(Cartwright 1978) as an alternative to the minimization schema for
completing the characterization of the function computed by a program.
The idea was to compute the computation sequence of a program ⊗P with a
related %2complete recursive program%1 ⊗C(P) and to show
metamathematically that for any program

!!j6:	%2(∀x)(f(x) = last f%4C(P)%2(x)%1

where %2f%4C(P)%1 is the function computed by ⊗C(P), and %2last%1 is a function
giving the last element of a list - in this case the list of values of ⊗f arising
in the computation.  Since whether %2C(P)%1
terminates for given arguments follows from its functional equation, ({eq j6})
allows us to establish this for ⊗P itself.  The constructions of
(Cartwright 1978) were somewhat involved and differed substantially
according to whether the original program was executed call-by-name or
call-by-value.

	The derived programs that give the number of recursions are complete
so that ⊗nrflat as defined above satisfies

!!j7:	%2(∀x u)(isint nrflat[x,u] ≡ issexp flat[x,u])%1.

	A program for the number of recursions done when a program is
evaluated call-by-name can also be given.  Thus the number of recursions
done in evaluating ⊗morris[m,n] call-by-name is given by ⊗cmorris[m,0,n,0] 
where 
.skip
.begin nofill
!!j8: ∂(8)%2cmorris[m,cm,n,cn] ← 
∂(12)1 + cm + qif m equal 0 qthen 0 qelse cmorris1[m-1,0,morris[m,n],cmorris[m,0,n,cn]]%1.
.end

The idea is that the arguments ⊗cm and ⊗cn are the numbers of recursive
calls involved in evaluating ⊗m and ⊗n respectively.
⊗morris and ⊗cmorris are again equi-terminating.
.skip 1
.bb "#. Proof Methods as Axiom Schemata"

	Representing recursive definitions in first order logic permits
us to express some well known methods for proving partial correctness
as axiom schemata of first order logic.

	For example, suppose we want to prove that if the input ⊗x of a
function ⊗f defined by

!!c1:	%2f x ← qif p x qthen x qelse f h x%1

satisfies %2%AF%2(x)%1, then if the function terminates, the output %2f(x)%1
will satisfy %AY%2(x,f(x))%1.  We appeal to the following %2axiom schema of
inductive assertions%1:

!!c2:	%2(∀x)(%AF%2(x) ⊃ q(x,x)) ∧ (∀x y)(q(x,y) ⊃ qif p x qthen %AY%2(x,y)
qelse q(x,%8 %2h y))
.nofill
		⊃ (∀x)(%AF%2(x) ∧ isD f x ⊃ %AY%2(x,f x))%1

.fill
where %2isD f x%1 is the assertion that %2f(x)%1 is in the nominal
range of the function definition, i.e. is an integer or an S-expression
as the case may be, and asserts that the computation terminates.
In order to use the schema, we must invent a suitable predicate %2q(x,y)%1,
and this is precisely the method of inductive assertions.
The schema is valid for all predicates %AF%1, %AY%1, and %2q%1, and a
similar schema can be written for any collection of mutually recursive
definitions that is iterative.

	The method of %2subgoal induction%1 for recursive programs
was introduced in
(Manna and Pnueli 1970), but they didn't give it a name.
Morris and Wegbreit (1977) name it, extend it somewhat,
and apply it to Algol-like programs.
Unlike %2inductive assertions%1, it isn't
limited to iterative definitions.  Thus, for the
recursive program

!!c3:	%2f%45%2 x ← qif p x qthen h x qelse g1 f%45%2 g2 x%1,

where ⊗p is assumed total, we have

!!c4:	%2(∀x)(p x ⊃ q(x,h x)) ∧ (∀x z)(¬p(x) ∧ q(g2 x,z) ⊃ q(x,g1 z)) ∧
(∀x)(%AF%2(x) ∧ q(x,z) ⊃ %AY%2(x,z))
.nofill
		⊃ (∀x)(%AF%2(x) ∧ isD(f(x)) ⊃ %AY%2(x,f(x)))%1
.fill

	We can express these methods as axiom schemata,
because we have the predicate %2isD%1 to express termination.
The minimization schema itself can be proved by subgoal induction.
We need only take %2%AF%2(x)_≡_%3true%1 and %AY%2(x,y)_≡_(y_=_%Af%2(x))%1
and %2q(x,y)_≡_(y_=_%Af%2(x))%1.

	General rules for going from a recursive program to what amounts
to the subgoal induction schema are given in
(Manna and Pnueli 1970) and (Morris and Wegbreit 1977);
we need only add a conclusion involving
the %2isD%1 predicate to the Manna's and Pnueli formula %2W%4P%1.

	However, we can characterize subgoal induction
as an axiom schema.  Namely, we define %At%2'[q]%1 as an extension of %At%1
mapping relations into relations.  Thus if

!!c5:	%2%At%2[f](x) = qif p x qthen h x qelse g1 f g2 x%1,

we have

!!c6:	%2%At%2'[q](x,y) ≡ qif p x qthen (y = h x) qelse ∃z.(q(g2 x,z) ∧ y = g1 z)%1.

In general we have

!!c7:	%2(∀xy)(%At%2'[q](x,y) ⊃ q(x,y)) ⊃ (∀x)(isD f x ⊃ q(x,f x))%1,

from which the subgoal induction rule follows immediately given the properties
of %AF%1 and %AY%1.  I am indebted to Wolfgang Polak (oral communication)
for help in elucidating this relationship.

%3WARNING%1: The rest of this section is somewhat conjectural.
There may be bugs.

	The extension %2qt'[q]%1 can be determined as follows:
Introduce into the logic the notion of a %2multi-term%1 which is formed in
the same way as a term but allows relations written as functions.
For the present we won't interpret them but merely give rules for
introducing them and subsequently eliminating them again to get
an ordinary formula.  Thus
we will write %2q%2<e>%1 where ⊗e is any term or multi-term.
We then form %2qt'[q]%1
exactly in the same way %2qt[f]%1 was formed.  Thus for the 91-function
we have

!!c8:	%2qt'[q](x) = qif x>100 qthen x-10 qelse q%2<q%2<x+11>>%1.

The pointy brackets indicate that we are "applying" a relation.
We now evaluate %2qt'[q](x,y)%1 formally as follows:
.begin nofill

!!c9: ∂(8)%2qt'[q](x,y)∂(24)≡ (qif x>100 qthen x-10 qelse q%2<q%2<x+11>>)(y)
∂(24)≡ qif x>100 qthen y = x-10 qelse q(q%2<x+11>,y)
∂(24)≡ qif x>100 qthen y = x-10 qelse ∃z.(q(x+11,z) ∧ q(z,y))%1.
.end

This last formula has no pointy brackets and is just the formula that would
be obtained by Manna and Pnueli or Morris and Wegbreit.  The rules are
as follows:

	(i) %2qt'[q](x)%1 is just like %2qt[f](x)%1 except that ⊗q replaces
⊗f and takes its arguments in pointy brackets.

	(ii) an ordinary term ⊗e applied to ⊗y becomes %2y_=_e%1.

	(iii) %2q%2<e>(y)%1 becomes %2q(e,y)%1.

	(iv) %2P(q%2<e>)%1 becomes %2∃z.q(e,z)_∧_P(z)%1 when
%2P(q%2<e>)%1 occurs positively in %2qt'[q](x,y)%1 and becomes
%2∀z.q(e,z)_⊃_P(z)%1 when the occurrence is negatve.
It is not evident whether an independent semantics can be given to
multi-terms.
.skip 2
.bb "#. Representations Using Finite Approximations."

	Our second approach to representing recursive programs
by first order formulas goes back to Goedel (1931, 1934) who showed
that primitive recursive functions could be so represented.  (Our
knowledge of Goedel's work comes from (Kleene 1952)).

.turn on "α"

	Kleene (1952) calls a partial function ⊗f %2representable%1 if there
is an arithmetic formula ⊗A with free variables ⊗x and ⊗y such
that

!!b1:	%2(∀x_y)((y_=_f(x))_≡_A)%1,

where an arithmetic formula is built up from integer constants and
variables using only addition, multiplication and bounded quantification.
Kleene showed that all partial recursive functions are representable.
The proof involves Goedel numbering possible computation sequences
and showing that the relation between sequences and their elements
and the steps of the computation are all representable.

	In Lisp less machinery is needed, because sequences
are Lisp data, and the relation between a sequence and its elements
is given by basic Lisp functions and by the %2≤↓L%1
axiomatized in section 6 by

!!b2:	%2(∀u v)(u ≤↓L v ≡ (u = v) ∨ ¬null v ∧ u ≤↓L qd v)%1.

	Starting with %2≤↓L%1 and the basic Lisp functions and
predicates we will define other Lisp predicates without recursion.

	First we define the well known Lisp function ⊗assoc whose usual
recursive definition is

!!b7:	%2assoc[x,w] ← qif qn w qthen qnil qelse qif x equal qaa w qthen qa w
qelse assoc[x, qd w]%1

or non-recursively
.begin nofill

!!b8: ∂(8)%2(∀y)(y = assoc[x,w] ≡ (∀u)(u ≤↓L w ⊃ qaa u ≠ x) ∧ y = qnil
∂(30)∨ (∃u)(u ≤↓L w ∧ x = qaa u ∧ y = qa u 
∂(36)∧ (∀v)(v ≤↓L w ∧ u <↓L v ⊃ qaa v ≠ x))%1
.end

	Now suppose that

!!b8a:	%2f x ← qt[f](x)%1

is a recursive program, i.e. qt is a continuous functional.  Our non-recursive
definition of ⊗f uses finite approximations to ⊗f, i.e. lists of pairs of
⊗(x . f(x)), where each pair can be computed from the functional qt using only
the pairs that follow it on the list.  Thus we define
.begin nofill

!!b4:	%2ok[qt](w) ← 
∂(12)qn w or 
∂(12)qda w = qt[(λx)(qif qn assoc[x,qd w] qthen qb qelse qd assoc[x,qd w])](qaa w) and ok[qt](qd w)%1,
.end

or non-recursively
.begin nofill

!!b5:	%2(∀w)(ok[qt](w) ≡ 
∂(14)(∀u)(u ≤↓L w ⊃ 
∂(18)[null u ∨ qda u = qt[(λx)(qif qn assoc[x,qd u] qthen qb qelse qd assoc[x,qd u])](qaa u)]))%1
.end

Now we can define %2y = f(x)%1 in terms of the existence of a suitable ⊗w, namely
.begin nofill

!!b6:	%2(∀x y)(y = f(x) ≡ 
∂(15)(∃w)(ok[qt](w) ∧ y = qt[(λx)(qif qn assoc[x,w] qthen qb qelse qd assoc[x,w])](x)))%1
.end

	It might be asked whether ≤↓L is necessary.  Couldn't we
represent recursive programs using just %2car, cdr, cons%1 and %2atom%1?
No, for the following reason.
Suppose that the function ⊗f is representable using only the basic Lisp
functions without ≤↓L, and consider the sentence

!!b12:	%2(∀x)(issexp_f(x))%1,

asserting the totality of ⊗f.  Using the representation, we can write ({eq b12})
as a sentence involving only the basic Lisp functions and the
constant qb.  However, Oppen (1978) has shown that these sentences are
decideable, and totality isn't.

	In case of functions of several variables,
({eq b6}) corresponds to a call-by-value
computation rule while the representations of the previous sections correspond
to call-by-name or other "safe" rules.
Treating call-by-name similarly requires a definition of ⊗ok in which
some of the tuplets have some missing elements.

Note: Our original intention was to take ≤↓S as basic, but curiously, we
have not succeeded in defining ≤↓L non-recursively in terms of ≤↓S, although
the converse is a consequence of our general construction.
.BB "#. Questions of Incompleteness."

	Luckham, Park and Paterson (1970) have shown that whether a
program schema diverges for every interpretation, whether it diverges
for some interpretation, and whether two program schemas are equivalent
are all not even partially solvable problems.  Manna (1974) has a
thorough discussion of these points.  In view of these results, what
can be expected from our first order representations?

	First let us construct a Lisp computation that does not terminate,
but whose non-termination cannot be proved from the axioms Lisp1 within
first order logic.  We need only program a proof-checker for first order
logic, set it to generate all possible proofs starting with the axioms Lisp1,
and stop when it finds a proof of (qnil ≠ qnil) or some other contradiction.
Assuming the axioms are consistent, the program will never find such a
proof and will never stop.  In fact, proving that the program will never
stop is precisely proving that the axioms are consistent.  But Goedel's
theorem asserts that axiom systems like Lisp1 cannot be proved consistent
within themselves.
Until recently, all the known cases of sentences of Peano arithmetic unprovable
within Peano arithmetic
involved such an appeal to Goedel's theorem
or similar unsolvability arguments.
However, Paris and Harrington (1977) found a form of Ramsey's theorem
a well-known combinatorial theorem,
that could be proved unprovable in Peano arithmetic.
However, their proof of its unprovability
involved showing that it implied the consistency of
Peano arithmetic.

	We can presumably prove Lisp1 consistent
just as Gentzen proved arithmetic consistent - by introducing
a new axiom schema that allows induction up to the transfinite ordinal
ε%40%1.  Proving the new system consistent would require induction up to
a still higher ordinal, etc.

	Since every recursively defined function can be defined explicitly,
any sentence involving such functions can be replaced by an equivalent
sentence involving only %2≤↓L%1 and the basic Lisp functions.
The theory of %2≤↓L%1 and these functions has a standard model, the
usual S-expressions and many non-standard models.  We "construct"
non-standard models in the usual way by appealing to the theorem that
if every finite subset of a set ⊗S of sentences of first order logic
has a model, then ⊗S has a model.
For example, take %2S = α{qnil %2≤↓L%* x, %1(A) %2≤↓L%* x, %1(A A)%2 %2≤↓L%* x,
, ...%1 indefinitelyα}.  Every finite subset of ⊗S has a model;
we need only take ⊗x to be the longest list of A's occurring in the
sentences.
Hence there is a model of the Lisp axioms in which ⊗x has all lists
of A's as subexpressions.  No sentence true in the standard model
and false in such a model can be proved from the axioms.  However,
it is necessary to be careful about the meaning of termination of a
function.  In fact, taking successive %2cdr%1s of such an ⊗x would
never terminate, but the sentence whose %2standard interpretation%1
is termination of the computation is provable from Lisp1.

	The practical question is: where does the correctness of ordinary
programs come in?  It seems likely that such statements will be provable
with our original system of axioms.  It doesn't follow that the system
Lisp1 will permit convenient proofs, but probably it will.  Some heuristic
evidence for this comes from (Cohen 1965).  Cohen presents two systems
of axiomatized arithmetic Z1 and Z2.  Z1 is ordinary Peano arithmetic with
an axiom schema of induction, and Z2 is an axiomatization of hereditarily
finite sets of integers.  Superficially, Z2 is more powerful than Z1, but
because the set operations of Z2 can be represented in Z1 as functions
on the Goedel numbers of the sets, it turns out that Z1 is just as powerful
once the necessary machinery has been established.  Because sets and lists
are the basic data of Lisp1, and sets are easily represented, the power of Lisp1
will be approximately that of Z2, and convenient proofs of correctness
statements should be possible.  
Moreover, since Lisp1 is a first order theory, it is easily extended
with axioms for sets, and this should help make informal proofs easy to
express.

%7	A PUB source of this paper is available on disk at the Stanford
Artificial Intelligence Laboratory with the file name FIRST[W79,JMC].%1
.bb "#. References."
.<<copies to Albert Meyer, Dana Scott>>

%3Bochvar, D.A. (1938)%1: "On a three-valued logical calculus and its
application to the analysis of contradictions", %2Recueil Mathematique%1,
N.S. 4 pp. 287-308.

%3Bochvar, D.A. (1943)%1: "On the consistency of a three-valued
logical calculus", %2Recueil Mathematique%1, N.S. 12, pp. 353-369.

The above Russian language papers by Bochvar are available in 
English translation as

%3Bochvar, D.A. (1972)%1: %2Two papers on partial predicate calculus%1,
Stanford Artificial Intelligence Memo 165, Computer Science Department,
Stanford University, Stanford, CA 94305.  (Also available from NTIS).

%3Cartwright, R.S. (1976)%1:
%2A Practical Formal Semantic Definition and Verification System
for Typed Lisp%1,
Ph.D. Thesis, Computer Science Department, Stanford University,
Stanford, California.

%3Cartwright, R. (1978)%1: %2First Order Semantics: A Natural
Programming Logic for Recursively Defined Functions%1, Cornell
University Computer Science Department Technical Report TR78-339,
Ithaca, New York.

%3Cartwright, Robert and John McCarthy (1979)%1: "First Order
Programming Logic", paper presented at the sixth annual ACM
Symposium on Principles of Programming Languages (POPL), San
Antonio, Texas.  Available from ACM.

%3Cohen, Paul (1966)%1: %2Set Theory and the Continuum Hypothesis%1,
W.A. Benjamin Inc.

%3Cooper, D.C. (1969)%1: "Program Scheme Equivalences and Second-order
Logic", in B. Meltzer and D. Michie (eds.), %2Machine Intelligence%1,
Vol. 4, pp. 3-15, Edinburgh University Press, Edinburgh.

%3Friedman, Daniel and David Wise(1976)%1: "Cons should not Evaluate
Its Arguments", in %2Proc. 3rd Intl. Colloq. on Automata, Languages
and Programming%1, Edinburgh Univ. Press, Edinburgh.

%3Hitchcock, P. and D. Park (1973)%1: "Induction Rules and Proofs of
Program Termination%1, in M. Nivat (ed.), %2Automata, Languages and
Programming%1, pp. 225-251, North-Holland, Amsterdam.

%3Kleene, S.C. (1952)%1: %2Introduction to Metamathematics%1,
Van Nostrand, New York.

%3Luckham, D.C., D.M.R.Park, and M.S. Paterson (1970)%1: "On Formalized
Computer Programs", %2J. CSS%1, %34%1(3): 220-249 (June).

%3Manna, Zohar and Amir Pnueli (1970)%1: "Formalization of the Properties
of Functional Programs", %2J. ACM%1, %317%1(3): 555-569.

%3Manna, Zohar (1974)%1: %2Mathematical Theory of Computation%1,
McGraw-Hill.

%3Manna, Zohar, Stephen Ness and Jean Vuillemin (1973)%1: "Inductive Methods
for Proving Properties of Programs", %2Comm. ACM%1,%316%1(8): 491-502 (August).

%3McCarthy, John (1963)%1: "A Basis for a Mathematical Theory of Computation", in
P. Braffort and D. Hirschberg (eds.), %2Computer Programming and Formal Systems%1,
pp. 33-70.  North-Holland Publishing Company, Amsterdam.

%3McCarthy, John (1964)%1: %2Predicate Calculus with "Undefined" as a
Truth Value%1, Stanford Artificial Intelligence Memo 1, Computer
Science Department, Stanford University.

%3McCarthy, John (1978)%1: 
"Representation of Recursive Programs in First Order Logic", in E.K. Blum and
S. Takasu (eds.) %2Proceedings of The International Conference on Mathematical
Studies of Information Processing%1, Kyoto.
(a preliminary and superseded version of this paper)

%3McCarthy, John and Carolyn Talcott (1979)%1: 
%2LISP: Programming and Proving%1,
(in preparation)

%3Morris, James H.(1968)%1: %2Lambda Calculus Models of Programming
Languages%1. Ph.D. Thesis, M.I.T., Cambridge, Mass.

%3Morris, James H., and Ben Wegbreit (1977)%1: "Program Verification
by Subgoal Induction", %2Comm. ACM%1,%320%1(4): 209-222 (April).

%3Oppen, Derek (1978)%1: %2Reasoning about Recursively Defined Data Structures%1,
Stanford Artificial Intelligence Memo 314, Computer
Science Department, Stanford University.

%3Paris, Jeff and Leo Harrington (1977)%1: "A Mathematical Incompleteness
in Peano Arithmetic", in Jon Barwise (ed.),
%2Handbook of Mathematical Logic%1, pp. 1133-1142.
North-Holland Publishing Company, Amsterdam.

%3Park, David (1970)%1: Fixpoint Induction and Proofs of Program
Properties", in %2Machine Intelligence 5%1, pp. 59-78, Edinburgh
University Press, Edinburgh.

%3Scott, Dana (1970)%1: %2Outline of a Mathematical Theory of Computation%1.
Programming Research Group Monograph No. 2, Oxford.

%3Takeuchi, I. (1978)%1: Personal Communication.

%3Vuillemin, J. (1973)%1: %2Proof Techniques for Recursive Programs%1. Ph.D.
Thesis, Stanford University, Stanford, Calif.